
%\newpage
To illustrate how
located and update processes
in our framework extend the expressiveness of session-typed languages, we  
revisit the  client/server scenario discussed in the Introduction:
% of distributed, interacting services (a client $C_1$ and a replicated service $S$), 
%conveniently represented as located processes:
\begin{eqnarray*}
\mathsf{Sys} & \triangleq &  %\scomponent{l_{0}}{C_1} \para 
%\scomponent{l_{1}}{C_1} \para\bigscomponent{l_2}{\scomponent{r}{S} \para R \, } \quad\text{where:} \vspace{3mm} \\ 
%C_1  &  \triangleq  & \nopenr{a}{c:\overline{\ST}}.\outC{c}{u_1,p_1}.\select{c}{n_1.P_1}.\close{c} \\
%S  &  \triangleq  & \repopen{a}{s:\ST}.\inC{s}{u,p}.\branch{s}{n_1{:}Q_1 \parallel n_2{:}Q_2}.\close{s} 
\scomponent{l_{1}}{C_1} \para\bigscomponent{l_2}{\scomponent{r}{S} \para R \, } \quad\text{where:} \vspace{3mm} \\ 
C_1  &  \triangleq  & \nopenr{a}{x}.\outC{x}{\mathrm{u_1},\mathrm{p_1}}.\select{x}{n_1.P_1}.\close{x} \\
S  &  \triangleq  & \repopen{a}{y}.\inC{y}{u,p}.\branch{y}{n_1{:}Q_1.\close{y} \alte n_2{:}Q_2.\close{y}} 
\end{eqnarray*}
%Intuitively, 
%$\mathsf{Sys}$ 
%consists of a server $S$ and a client $C_1$.
%They 
%may interact by establishing a session %of type $\sigma$ 
%%between $S$ and $C_1$ %($i \in \{0, 1\}$) 
%using name $a$:
%first, the client sends its user credentials to the server; then, the client chooses one of the two
%services offered by the server. 
%Above, the actual client and server behaviors are  abstracted by processes $P_1$ and $Q_1$, respectively,
%%(resp. $P_1$ and $Q_1$), 
%which are left unspecified.
%Finally, server and client synchronize to close the session.

Recall that process $R$ above represents the platform in which service $S$ is deployed.
We now discuss two
different definitions for $R$:
this is useful to illustrate  the different facets that runtime adaptation may adopt in our typed framework.

In what follows, we assume that $Q_i$ realizes a  behavior denoted by type $\beta_i$ ($i \in \{1,2\}$),
and write $\alpha$ to stand for the session type $?(\tau_1,\tau_2).\&\{n_1: \beta_1, n_2: \beta_2\}$ for the server $S$.
Dually, the type for $C_1$ is $\overline{\alpha} = !(\tau_1,\tau_2).\oplus\{n_1: \overline{\beta_1}, n_2: \overline{\beta_2}\}$;
we assume that $P_1$ realizes the session type  $\overline{\beta_1}$.
  
  
%\todo{change $c, s$ with $x$ and say what's $\alpha$.}

\subsection{A Basic Service Reconfiguration: Relocation and Upgrade}
%Here we develop an $R$ which keeps the distributed structure, but adds another service to the menu.
We first suppose that $R$ stands for a simple adaptation routine for $S$ which 
(i)~relocates the service from $r$ to $l_4$, and 
(ii)~sets up a new adaptation routine at $l_4$ which upgrades $S$ with adaptation mechanisms for $Q_1$ and $Q_2$ (denoted $R_{11}$ and $R_{12}$, respectively, and left unspecified):
\begin{eqnarray*}
R & \triangleq &  \adapt{r}{ \scomponent{l_4}{\mathsf{X}}   \para \adapt{l_4}{\scomponent{l_4}{S_{\text{new}}}}{\mathsf{X}_1} \, }{\mathsf{X}}~ \qquad\text{where:} \\
S_\text{new}  &  \triangleq  & \repopen{a}{y}.\inC{y}{u,p}.\branch{y}{n_1{:}Q^*_1.\close{y} \alte n_2{:}Q^*_2.\close{y}\,}  \\
Q^*_1 & \triangleq &  \scomponent{l_5}{Q_1} \para \adapt{l_5}{R_{11}}{\mathsf{X}_2} \\
Q^*_2 & \triangleq &  \scomponent{l_6}{Q_2} \para \adapt{l_6}{R_{12}}{\mathsf{X}_3}
\end{eqnarray*}
It is easy to see that the only difference between $S$ and $S_\text{new}$ is in the behavior given at label $n_2$---for 
simplicity, we assume that $Q_2$ and $Q^*_2$ are implementations of the same typed behavior.
For this $R$, using our type system, we can infer that 
$$
\judgebis{\env{\Gamma}{\Theta}}{\mathsf{Sys}}{\type{\emptyset}{\INT_1}} \qquad \text{where:}
$$

\begin{itemize}
\item $\{ a: \langle \ST_\quau, \overline{\ST}_\qual \rangle \} \subseteq \Gamma$
\item $\{ l_1\mapsto a:\overline{\ST}_\qual,~ 
l_4\mapsto a:\ST_\quau, ~ r\mapsto a: \ST_\quau , ~ \mathsf{X} \mapsto a: \ST_\quau  \} \subseteq \Theta$
\item $ \INT_1 = \{ \qual\,a:\overline{\ST},  ~ \quau\,a:\ST \} $ %CHECK HERE
\end{itemize}
and where we have\done\todo[B39.]{Fixed, pls check} slightly simplified notation for $\Theta$, for readability reasons.

By virtue of Theorem~\ref{t:safety}
typing ensures communications between $C_1$ and $S$ which follow the prescribed session types. Moreover, 
by relying on Theorem~\ref{t:consist}, we know that well-typedness implies consistency, i.e., % between $C$ and $S$, i.e., 
an update action on  $r$ will not be enabled if $C_1$ and $S$ have already initiated a session.
For the scenario above, 
our typed framework ensures that  updates may only take place before a session related to the service on $a$ is established.
Suppose such an action occurs as the first action of $\mathsf{Sys}$ (i.e. service $S$ is immediately relocated, from $r$ to $l_4$): 
$$
\mathsf{Sys} \pired 
%\component{l_{0}}{0}{}{C_0} \para
\component{l_{1}}{0}{}{C_1} \para 
\bigcomponent{l_2}{0}{}{\component{l_4}{0}{}{S}  \para \adapt{l_4}{\scomponent{l_4}{S_\text{new}}}{{\mathsf{X}_1}} \,} 
%\pired \component{l_{0}}{0}{}{C_0} \para \component{l_{1}}{0}{}{C_1} \para \bigcomponent{l_2}{0}{}{\component{l_4}{0}{}{S_\text{new}}  \,}  
= \mathsf{Sys}_1
$$
The above reduction represents one of the simplest forms of reconfiguration, one in which the behavior of the located process
is not explicitly changed. 
Still, we observe that runtime relocation may \emph{indirectly}\done\todo[B40.]{Fixed, pls check} influence the future behavior of a process.
For instance, after relocation the process may 
synchronize with reconfiguration routines (i.e., update processes) not defined for the previous location.
This is exactly what occurs with the above definition for $R$ when relocating $S$ to $l_4$---see below.\footnote{
Conversely, 
update actions that 
remove the enclosing location(s) for a process, or 
relocate it to a location on which there are no update processes available are two ways of preventing future updates.}
Also, the new location may be associated to a larger interface (wrt $\sqsubseteq$) and this could be useful to eventually
enable reconfiguration steps not possible for the process in the old location.

Starting from $\mathsf{Sys}_1$, the service $S$ can be then upgraded to $S_\text{new}$ by synchronizing on $l_4$. We may have:
$$
\mathsf{Sys}_1 
%\pired \component{l_{0}}{0}{}{C_0} \para \component{l_{1}}{0}{}{C_1} \para \bigcomponent{l_2}{0}{}{\component{r_1}{0}{}{S_\text{new}}  \para \adaptn{r}{\scomponent{l_4}{\mathsf{X}}} \,} 
\pired %\component{l_{0}}{0}{}{C_0} \para 
\component{l_{1}}{0}{}{C_1} \para \bigcomponent{l_2}{0}{}{\component{l_4}{0}{}{S_\text{new}}  \,}  = \mathsf{Sys}_2
$$
and by Theorem~\ref{th:subred} we infer that 
$$
\judgebis{\env{\Gamma}{\Theta}}{\mathsf{Sys}_2}{\type{\emptyset}{\INT_1}}
$$

\subsection{Upgrading Behavior and Distributed Structure}\label{ss:behdist}
Suppose now that $R$ stands for the following adaptation routine for $S$:
$$
\begin{array}{ll}
R & \triangleq   \adapt{r}{\scomponent{r_1}{S_\text{wra}}  \para \scomponent{r_2}{S_\text{rem}} }{{\mathsf{X}}}~ \qquad\text{where:} \\
%S_\text{wra}  &  \triangleq  & \repopen{a}{s:\ST}.\nopenr{b}{d:!(\ST)}.\throw{d}{s}.\close{d} \\
%S_\text{rem} &  \triangleq  &  \repopen{b}{e:?(\ST)}.\catch{e}{s}.\inC{s}{u,p}.\branch{s}{n_1{:}Q_1 \parallel n_2{:}Q_2}.\close{s}.\close{e} 
S_\text{wra} \! \! \! \!&  \triangleq   \repopen{a}{x}.\nopenr{b}{y}.\throw{y}{x}.\close{y} \\
S_\text{rem} \! \! \! \!&  \triangleq    \repopen{b}{z}.\catch{z}{x}.\inC{x}{u,p}.\branch{x}{n_1{:}Q_1.\close{x}.\close{z}  \alte %\\
%& 
%\qquad \qquad \qquad \qquad \qquad \qquad  \quad \qquad 
n_2{:}Q_2.\close{x}.\close{z} }
\end{array}
$$
Above, $S_\text{wra}$ represents a service wrapper which, deployed at $r_1$, acts as a mediator: 
it redirects all client requests on name $a$ 
to the remote service $S_\text{rem}$, defined on name $b$ and deployed at $r_2$. 
Although simple, this service structure is quite appealing: 
by exploiting session delegation, 
it hides 
from clients certain implementation details (e.g.,  name $b$ and location $r_2$), 
therefore simplifying  future reconfiguration tasks---in fact, clients do not need to know about $b$ to execute, and so $S_\text{wra}$ can be transparently upgraded.
This new definition for $R$ illustrates\done\todo[B41.]{Fixed, pls check} an update process that may reconfigure both
the behavior and distributed structure of $S$:
in a single step, 
the monolithic service $S$ is replaced by a more flexible distributed
implementation based on  $S_\text{wra}$ and $S_\text{rem}$ and deployed at $r_1$ and $r_2$ (rather than at $r$).
As we discuss below, $R$ above does not involve process variables, and so the current behavior at $r$ is discarded.
Using our type system, we may infer that 
$$
\judgebis{\env{\Gamma}{\Theta}}{\mathsf{Sys}}{\type{\emptyset}{\INT_1}} \qquad \text{where:}
$$

\begin{itemize}
\item $\{ a: \langle \ST_\quau, \overline{\ST}_\qual \rangle,~  
b: \langle !(\ST)_\qual, ?(\ST)_\quau \rangle \} \subseteq \Gamma$
\item $\{ l_1\mapsto a:\overline{\ST}_\qual,~ 
l_2\mapsto a:\ST_\quau \cup b: !(\ST)_\quau \cup b: ?(\ST)_\quau, ~
r\mapsto a: \ST_\quau, ~ 
r_1\mapsto \ST_\quau \cup b: !(\ST)_\quau,~ \\
r_2\mapsto b: ?(\ST)_\quau
\} \subseteq \Theta$
\item $ \INT_1 = \{  \qual\,a:\overline{\ST},  ~ \quau\,a:\ST \} $ %CHECK HERE
\end{itemize}
and where we have\done\todo[B42.]{Fixed, pls check} slightly simplified notation for $\Theta$, for readability reasons.

As before,  our typed framework ensures that 
consistent updates may only take place before a session related to the service on $a$ is established.
Suppose such an action occurs as the first action of $\mathsf{Sys}$ (i.e. the definition of service $S$ is immediately updated): %before a session on $a$ is established. 
$$
\mathsf{Sys} \pired 
%\component{l_{0}}{0}{}{C_0} \para
\component{l_{1}}{0}{}{C_1} \para \bigcomponent{l_2}{0}{}{\component{r_1}{0}{}{S_\text{wra}}  \para \component{r_2}{0}{}{S_\text{rem}}} = \mathsf{Sys}'
$$
Because $R$ declares no process variables, this step
formalizes an update operation which \emph{discards} the behavior located at $r$ (i.e., $a: \alpha_\quau$).
To understand why this reconfiguration step is safe, it is crucial to observe that:
\begin{enumerate}[(i)] 
\item  the new service implementation, based on $S_\text{wra}$ and $S_\text{rem}$, respects the prescribed interfaces of the involved locations (i.e., $r_1$ and $r_2$, not used in $\mathsf{Sys}$); 
\item  the interface of location $l_2$ (which hosts the server implementation) can indeed contain the two services on name $b$ implemented by $S_\text{wra}$ and $S_\text{rem}$.
\end{enumerate}
These two important conditions are statically checked by our typing system.
After the reduction it is easy to see that 
$$
\judgebis{\env{\Gamma}{\Theta}}{\mathsf{Sys}'}{\type{\emptyset}{\INT_2}} 
$$
where $\Gamma, \Theta$ are as above and $\INT_2 = \{ \qual \, a:\overline{\ST},~\quau \, a:\ST,~\quau \, b: ?(\ST), ~\quau \, b: !(\ST)\}$.
We have $\INT_1 \sqsubseteq \INT_2$: indeed the interface grows as \done\todo[B43.]{Fixed as suggested, pls check}the updated service  now relies on two service definitions (on names $a, b$) rather than on a single  definition.

%\jp{Other ideas for extending the example?}


%\subsection{More interesting server}
%
%
%We consider the interaction between a Client and a Server as the process $S \parallel C$. 
%The behavior of the server is encoded trough an adaptable process that recursively establishes new sessions with clients:
%$$ S ::= \component{s}{0}{\Delta}{\rec{X:\emptyset, \Delta}{(\open{c:\rho}.c(x).\close{c} \parallel X)} }$$ 
%where $\Delta= \emptyset \shortmid \{\rho\}$ and $\rho = ?(int).\epsilon$.
%
%Clients, in order to connect to the server, must implement a session that is the dual of the one described above: 
%$$C ::= \open{c:\overline{\rho}}.\outC{c}{e}.\close{c}$$
%where $e$ is an expression that evaluates to  $int$.
%
%We now extend this scenario introducing a way of updating the server: $S \parallel C \parallel U$. Here, the update $U$ is meant to extend  the capabilities (for instance by enhancing its performance) of the server by adding an auxiliary machine $M$. The server is then delegating its sessions to $M$:
%$$
%\begin{array}{ll}
%U ::= & \updated{s}{X}{\Delta}{\Delta}{(\component{s}{0}{\Delta}{\rec{X:\emptyset, \Delta}{(\open{c:\rho}.\\
%& \qquad \qquad \open{d:\sigma}.\throw{d}{c}.\close{d}} \parallel X)} \parallel M)}\\
%M ::= &\component{m}{0}{\Delta'}{\rec{X:\emptyset, \Delta'}{(\open{d:\overline{\sigma}}.\catch{d}{e}.\\
%&  \qquad \qquad e(x).\close{e}.\close{d} \parallel X)}}
%\end{array}
% $$
%where $\Delta' = \emptyset \shortmid \ \{\overline{\sigma}\}$ and $\sigma = !(\rho).\epsilon$.




  

%T = open 